$\vdash$  $\forall$$T$:Type, $x$,$y$:$T$. ($x$ = $y$) $\Leftarrow\!\Rightarrow$ ($y$ = $x$)